; EXPECT: unsat
(set-logic ALL)
(set-option :incremental false)
(declare-fun x1 () Real)
(declare-fun x2 () Real)
(declare-fun y1 () Real)
(declare-fun y2 () Real)
(declare-fun f (Real) Real)
(declare-fun g (Real Real) Real)
(assert (and (<= x1 x2) (<= x2 x1)))
(assert (not (= (g x1 y1) (g x2 y2))))
(assert (let ((_let_1 (f x1))) (and (<= y1 _let_1) (<= _let_1 y1))))
(assert (let ((_let_1 (f x2))) (and (<= y2 _let_1) (<= _let_1 y2))))
(check-sat)
